
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{ArithEval} (\coqdocvar{s}: \coqdocvar{State}) : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{Integer} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_eval\_num}   : \coqdockw{\ensuremath{\forall}} (\coqdocvar{n}:\coqdocvar{Integer}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} (\coqdocvar{arith\_exp\_num} \coqdocvar{n}) \coqdocvar{n}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_eval\_id}    : \coqdockw{\ensuremath{\forall}} (\coqdocvar{i}:\coqdocvar{Id})(\coqdocvar{z}:\coqdocvar{Integer}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{s} \coqdocvar{i} = \coqdocvar{Some} (\coqdocvar{int\_val} \coqdocvar{z}) \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} (\coqdocvar{arith\_exp\_id} \coqdocvar{i})  \coqdocvar{z}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_eval\_plus}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp}) (\coqdocvar{n1} \coqdocvar{n2} : \coqdocvar{Integer}), \coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} (\coqdocvar{arith\_exp\_plus} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_plus} \coqdocvar{n1} \coqdocvar{n2}) \coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_eval\_minus} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp}) (\coqdocvar{n1} \coqdocvar{n2} : \coqdocvar{Integer}), \coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} (\coqdocvar{arith\_exp\_minus} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_minus} \coqdocvar{n1} \coqdocvar{n2}) \coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_eval\_mult}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp}) (\coqdocvar{n1} \coqdocvar{n2} : \coqdocvar{Integer}), \coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} (\coqdocvar{arith\_exp\_mult} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_mult} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_eval\_div}   : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp}) (\coqdocvar{n1} \coqdocvar{n2} : \coqdocvar{Integer}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} (\coqdocvar{arith\_exp\_div} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_div} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_eval\_mod}   : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp}) (\coqdocvar{n1} \coqdocvar{n2} : \coqdocvar{Integer}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} (\coqdocvar{arith\_exp\_mod} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_modulo} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}